ELF[2]

Robert Harper and Frank Pfenning, Carnegie Mellon University

A constraint-logic programming language based on the LF logical framework. Intended as a metalanguage for the specification, implementation and proving properties of programming languages and logics. Implemented in Standard ML of New Jersey.